1.1 Field of the Invention
The invention pertains to artificial intelligence systems generally and more specifically to artificial intelligence systems that perform inference in the context of large knowledge bases. In this context, a theory is a set of logical formulas which represent knowledge about a problem of interest. Given a theory, an artificial intelligence system can make new inferences for a user of the system. The user may be an individual or another system, and is termed herein an agent.
1.2 Description of the Prior Art
Generally speaking, the formulas in a knowledge base are written in predicate calculus. Such formulas may con,in logical quantifiers such as "there exists" or "for all" , logical operators such as "and" , "or" , "implies" , or "not" , "predicates", which express properties of individuals or objects, variables, which represent individuals or objects in the world without explicitly naming them, constants, which are explicit names for individuals or objects, and functions which allow reference to individuals or objects in terms of others. A term is a variable, a constant, or the application of a function to another term; a ground term is a term with no variables. A quantified formula is a formula containing a first-order quantifier ( or ). A rule is a formula containing one or more variables whose top-level connective is . The antecedent and consequent of a rule are defined in the obvious way. A fact is a formula containing neither quantifiers nor variables.) For details of predicate calculus see (Genesereth, M. R., and Nilsson, N. J. Logical Foundations of Artificial Intelligence. Morgan Kaufman. 1987.).
Traditional predicate calculus is monotonic--if a set of formulas Th in predicate calculus implies a conclusion c then any superset Th' of Th also implies c. In practical terms, this means that a conclusion, once made, will never have to be revised as a consequence of further reasoning.
Unfortunately, many of the types of reasoning required in advanced applications of artificial intelligence have aspects that are inherently not monotonic. Nonmonotonic logics do not have the property that a conclusion will never have to be revised--in such logics it may be the case that Th implies c but a superset, Th', does not imply c. Nonmonotonic logics thus have some of the properties of human common-sense reasoning: that is, a reasonable conclusion is made based on the information and inferences presently available, and that conclusion is revised if further information or further deliberation about the problem indicate that revision is required. For a general overview of monotonic and nonmonotonic logic and their use in artificial intelligence see (Genesereth, M. R., and Nilsson, N. J. Logical Foundations of Artificial Intelligence. Morgan Kaufman. 1987.).
In general, nonmonotonic formalisms sanction default conclusions only if certain formulae can be shown to be consistent with the rest of the system's beliefs. (In logic a formula is consistent with a set of beliefs if there is some possible state of the world (a model) in which both the theory and the set of beliefs are true.) For example, in default logic the justification of a default must be shown to be consistent with all other beliefs before the consequent is sanctioned; similarly, in closed-world reasoning, P can be assumed only if P does not follow. Unfortunately, in the worst case, consistency is even harder to determine than logical consequence. While the theorems of a first-order theory are recursively enumerable, there can be no effective procedure to determine first-order consistency. In most cases, the unacceptable time complexity of nonmonotonic formalisms can be traced to this consistency check.
It is striking how much early work on nonmonotonic reasoning was motivated by the idea that defaults should make reasoning easier. For example, Reiter (Reiter, R. 1978. On reasoning by default. In Proceedings of the Second Conference on Theoretical Issues in Natural Language Processing, Urbana, Ill. 210-218.) says "[the closed-world default] leads to a significant reduction in the complexity of both the representation and processing of knowledge". Winograd (Winograd, T. 1980. Extended inference modes in reasoning by computer systems. Artificial Intelligence 13:5-26.) observes that the nature of the world is such that mechanisms for making assumptions are necessary for an agent to act in real time: "A robot with common sense would begin an automobile trip by walking to the place where it expects the car to be, rather than sitting immobilized, thinking about the infinite variety of ways in which circumstances may have conspired for it not to be there. From a formal point of view, there is no way to prove that it is still there, but nevertheless one must act, and must do so on the basis of plausible assumptions."
Paradoxically, formal theories of nonmonotonic reasoning have been consistently characterized by their intractability. For example, first-order default logic (Reiter, R. 1980. A logic for default reasoning. Artificial Intelligence 13:81-132.) is not semi-decidable and its rules of inference are not effective--it might take forever (not just a very long time) to determine that something is a consequence of a default theory. Even very restricted sublanguages based on propositional languages with linear decision procedures remain NP-complete (Kautz, H. and Selman, B. 1989. Hard problems for simple default logics. In Proceedings, First International Conference on Principles of Knowledge Representation and Reasoning, Toronto, Canada. Morgan Kaufmann.). Convincing examples of useful theories within demonstrably tractable sublanguages for nonmonotonic reasoning have yet to appear. It is an object of the techniques disclosed herein to provide solutions to these and other problems involved in the use of nonmonotonic reasoning in artificial intelligence systems and thereby to provide more efficient artificial intelligence systems.